perm filename DLO1[1,JRA] blob sn#005805 filedate 1972-08-14 generic text, type T, neo UTF8
00100	LE1(X1 X2) ∨ LE1(X2 X1);
00200	(LE1(X1 X2) ∧ LE1(X2 X1))→ E(X1 X2);
00300	(LE1(X1 X2) ∧ LE1(X2 X3)) → LE1(X1 X3);
00400	LE1(X1 ADD1(X1));
00500	¬E(X1 ADD1(X1));
00600	LE1(X2 X1) ∨ LE1(ADD1(X1) X2);
00700	LE1(X1 X1);
00800	;